\begin{tabbing}
insert{-}by(${\it eq}$;$r$;$x$;$l$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=rec{-}case($l$) of [] =$>$ [$x$] $\mid$ $a$::${\it as}$ =$>$ $v$.if\= ${\it eq}$($x$,$a$)\+\+
\\[0ex]then [$a$ / ${\it as}$]
\-\\[0ex]if $r$($x$,$a$) then [$x$; $a$ / ${\it as}$] else [$a$ / $v$] fi 
\-
\end{tabbing}